CPAchecker Report

Find only exact matches

Matches in value-assignements (V): {{numOfValueMatches}}

Matches in edge-description: {{numOfDescriptionMatches}}

	Rank	Scope
-V-		{{line.bestrank}}		{{line.desc}}

Precondition (initial variable assignment):

{{fault.rank}}.

Details:

Current values:

Name	Value

{{sourceFiles[selectedSourceFile]}}

// Automatically generated by cegarmc  
//  
  
  
extern void __VERIFIER_assume(int);  
extern int __VERIFIER_nondet_bool();  
extern char __VERIFIER_nondet_char();  
extern signed char __VERIFIER_nondet_schar();  
extern unsigned char __VERIFIER_nondet_uchar();  
extern int __VERIFIER_nondet_int();  
extern unsigned int __VERIFIER_nondet_uint();  
extern short __VERIFIER_nondet_short();  
extern unsigned short __VERIFIER_nondet_ushort();  
extern long __VERIFIER_nondet_long();  
extern unsigned long __VERIFIER_nondet_ulong();  
extern long long __VERIFIER_nondet_longlong();  
extern unsigned long long __VERIFIER_nondet_ull();  
extern float __VERIFIER_nondet_float();  
extern double __VERIFIER_nondet_double();  
extern long double __VERIFIER_nondet_longdouble();  
extern void * __VERIFIER_nondet_pointer();  
  
int D_print_i;  
int D_print_st;  
int D_z;  
int N_generate_i;  
int N_generate_st;  
int S1_addsub_i;  
int S1_addsub_st;  
int S2_presdbl_i;  
int S2_presdbl_st;  
int S3_zero_i;  
int S3_zero_st;  
int count;  
int main_clk_ev;  
int main_clk_neg_edge;  
int main_clk_pos_edge;  
int main_clk_req_up;  
int main_clk_val;  
int main_clk_val_t;  
int main_dbl_ev;  
int main_dbl_req_up;  
int main_dbl_val;  
int main_dbl_val_t;  
int main_diff_ev;  
int main_diff_req_up;  
int main_diff_val;  
int main_diff_val_t;  
int main_in1_ev;  
int main_in1_req_up;  
int main_in1_val;  
int main_in1_val_t;  
int main_in2_ev;  
int main_in2_req_up;  
int main_in2_val;  
int main_in2_val_t;  
int main_pres_ev;  
int main_pres_req_up;  
int main_pres_val;  
int main_pres_val_t;  
int main_sum_ev;  
int main_sum_req_up;  
int main_sum_val;  
int main_sum_val_t;  
int main_zero_ev;  
int main_zero_req_up;  
int main_zero_val;  
int main_zero_val_t;  
int modFlag;  
int res;  
  
void error();  
void N_generate();  
void S1_addsub();  
void S2_presdbl();  
void S3_zero();  
void D_print();  
void eval();  
void start_simulation();  
  
  
void error() {  
  {  
  goto ERROR;  
  ERROR: ;  
  return;  
  }  
}  
  
void N_generate() {  
  auto int a;  
  auto int b;  
  {  
    main_in1_val_t = __VERIFIER_nondet_int();  
  main_in1_req_up = 1;  
    main_in2_val_t = __VERIFIER_nondet_int();  
  main_in2_req_up = 1;  
  return;  
  }  
}  
  
void S1_addsub() {  
  auto int a;  
  auto int b;  
  {  
  a = main_in1_val;  
  b = main_in2_val;  
  main_sum_val_t = a + b;  
  main_sum_req_up = 1;  
  main_diff_val_t = a - b;  
  main_diff_req_up = 1;  
  return;  
  }  
}  
  
void S2_presdbl() {  
  auto int a;  
  auto int b;  
  auto int c;  
  auto int d;  
  {  
  a = main_sum_val;  
  b = main_diff_val;  
  main_pres_val_t = a;  
  main_pres_req_up = 1;  
  c = a + b;  
  d = a - b;  
  main_dbl_val_t = c + d;  
  main_dbl_req_up = 1;  
  return;  
  }  
}  
  
void S3_zero() {  
  auto int a;  
  auto int b;  
  {  
  a = main_pres_val;  
  b = main_dbl_val;  
  main_zero_val_t = b - (a + a);  
  main_zero_req_up = 1;  
  return;  
  }  
}  
  
void D_print() {  
  {  
  D_z = main_zero_val;  
  return;  
  }  
}  
  
void eval() {  
  auto int tmp;  
  auto int tmp___0;  
  auto int tmp___1;  
  auto int tmp___2;  
  auto int tmp___3;  
  {  
  {  
    while (1) {  
      {  
        while_0_continue: ;  
        if (N_generate_st == 0) {  
          }  
        else {  
          if (S1_addsub_st == 0) {  
            }  
          else {  
            if (S2_presdbl_st == 0) {  
              }  
            else {  
              if (S3_zero_st == 0) {  
                }  
              else {  
                if (D_print_st == 0) {  
                  }  
                else {  
                  goto while_0_break;  
                  }  
                }  
              }  
            }  
          }  
        if (N_generate_st == 0) {  
          {  
                        tmp = __VERIFIER_nondet_int();  
            }  
          if (tmp) {  
            N_generate_st = 1;  
                        N_generate();  
            }  
          else {  
            }  
          }  
        else {  
          }  
        if (S1_addsub_st == 0) {  
          {  
                        tmp___0 = __VERIFIER_nondet_int();  
            }  
          if (tmp___0) {  
            S1_addsub_st = 1;  
                        S1_addsub();  
            }  
          else {  
            }  
          }  
        else {  
          }  
        if (S2_presdbl_st == 0) {  
          {  
                        tmp___1 = __VERIFIER_nondet_int();  
            }  
          if (tmp___1) {  
            S2_presdbl_st = 1;  
                        S2_presdbl();  
            }  
          else {  
            }  
          }  
        else {  
          }  
        if (S3_zero_st == 0) {  
          {  
                        tmp___2 = __VERIFIER_nondet_int();  
            }  
          if (tmp___2) {  
            S3_zero_st = 1;  
                        S3_zero();  
            }  
          else {  
            }  
          }  
        else {  
          }  
        if (D_print_st == 0) {  
          {  
                        tmp___3 = __VERIFIER_nondet_int();  
            }  
          if (tmp___3) {  
            D_print_st = 1;  
                        D_print();  
            }  
          else {  
            }  
          }  
        else {  
          }  
        }  
      }  
    while_0_break: ;  
    }  
  return;  
  }  
}  
  
void start_simulation() {  
  auto int kernel_st;  
  {  
  kernel_st = 0;  
  if (main_in1_req_up == 1) {  
    if (main_in1_val != main_in1_val_t) {  
      main_in1_val = main_in1_val_t;  
      main_in1_ev = 0;  
      }  
    else {  
      }  
    main_in1_req_up = 0;  
    }  
  else {  
    }  
  if (main_in2_req_up == 1) {  
    if (main_in2_val != main_in2_val_t) {  
      main_in2_val = main_in2_val_t;  
      main_in2_ev = 0;  
      }  
    else {  
      }  
    main_in2_req_up = 0;  
    }  
  else {  
    }  
  if (main_sum_req_up == 1) {  
    if (main_sum_val != main_sum_val_t) {  
      main_sum_val = main_sum_val_t;  
      main_sum_ev = 0;  
      }  
    else {  
      }  
    main_sum_req_up = 0;  
    }  
  else {  
    }  
  if (main_diff_req_up == 1) {  
    if (main_diff_val != main_diff_val_t) {  
      main_diff_val = main_diff_val_t;  
      main_diff_ev = 0;  
      }  
    else {  
      }  
    main_diff_req_up = 0;  
    }  
  else {  
    }  
  if (main_pres_req_up == 1) {  
    if (main_pres_val != main_pres_val_t) {  
      main_pres_val = main_pres_val_t;  
      main_pres_ev = 0;  
      }  
    else {  
      }  
    main_pres_req_up = 0;  
    }  
  else {  
    }  
  if (main_dbl_req_up == 1) {  
    if (main_dbl_val != main_dbl_val_t) {  
      main_dbl_val = main_dbl_val_t;  
      main_dbl_ev = 0;  
      }  
    else {  
      }  
    main_dbl_req_up = 0;  
    }  
  else {  
    }  
  if (main_zero_req_up == 1) {  
    if (main_zero_val != main_zero_val_t) {  
      main_zero_val = main_zero_val_t;  
      main_zero_ev = 0;  
      }  
    else {  
      }  
    main_zero_req_up = 0;  
    }  
  else {  
    }  
  if (main_clk_req_up == 1) {  
    if (main_clk_val != main_clk_val_t) {  
      main_clk_val = main_clk_val_t;  
      main_clk_ev = 0;  
      if (main_clk_val == 1) {  
        main_clk_pos_edge = 0;  
        main_clk_neg_edge = 2;  
        }  
      else {  
        main_clk_neg_edge = 0;  
        main_clk_pos_edge = 2;  
        }  
      }  
    else {  
      }  
    main_clk_req_up = 0;  
    }  
  else {  
    }  
  if (N_generate_i == 1) {  
    N_generate_st = 0;  
    }  
  else {  
    N_generate_st = 2;  
    }  
  if (S1_addsub_i == 1) {  
    S1_addsub_st = 0;  
    }  
  else {  
    S1_addsub_st = 2;  
    }  
  if (S2_presdbl_i == 1) {  
    S2_presdbl_st = 0;  
    }  
  else {  
    S2_presdbl_st = 2;  
    }  
  if (S3_zero_i == 1) {  
    S3_zero_st = 0;  
    }  
  else {  
    S3_zero_st = 2;  
    }  
  if (D_print_i == 1) {  
    D_print_st = 0;  
    }  
  else {  
    D_print_st = 2;  
    }  
  if (main_in1_ev == 0) {  
    main_in1_ev = 1;  
    }  
  else {  
    }  
  if (main_in2_ev == 0) {  
    main_in2_ev = 1;  
    }  
  else {  
    }  
  if (main_sum_ev == 0) {  
    main_sum_ev = 1;  
    }  
  else {  
    }  
  if (main_diff_ev == 0) {  
    main_diff_ev = 1;  
    }  
  else {  
    }  
  if (main_pres_ev == 0) {  
    main_pres_ev = 1;  
    }  
  else {  
    }  
  if (main_dbl_ev == 0) {  
    main_dbl_ev = 1;  
    }  
  else {  
    }  
  if (main_zero_ev == 0) {  
    main_zero_ev = 1;  
    }  
  else {  
    }  
  if (main_clk_ev == 0) {  
    main_clk_ev = 1;  
    }  
  else {  
    }  
  if (main_clk_pos_edge == 0) {  
    main_clk_pos_edge = 1;  
    }  
  else {  
    }  
  if (main_clk_neg_edge == 0) {  
    main_clk_neg_edge = 1;  
    }  
  else {  
    }  
  if (main_clk_pos_edge == 1) {  
    N_generate_st = 0;  
    }  
  else {  
    }  
  if (main_clk_pos_edge == 1) {  
    S1_addsub_st = 0;  
    }  
  else {  
    }  
  if (main_clk_pos_edge == 1) {  
    S2_presdbl_st = 0;  
    }  
  else {  
    }  
  if (main_clk_pos_edge == 1) {  
    S3_zero_st = 0;  
    }  
  else {  
    }  
  if (main_clk_pos_edge == 1) {  
    D_print_st = 0;  
    }  
  else {  
    }  
  if (main_in1_ev == 1) {  
    main_in1_ev = 2;  
    }  
  else {  
    }  
  if (main_in2_ev == 1) {  
    main_in2_ev = 2;  
    }  
  else {  
    }  
  if (main_sum_ev == 1) {  
    main_sum_ev = 2;  
    }  
  else {  
    }  
  if (main_diff_ev == 1) {  
    main_diff_ev = 2;  
    }  
  else {  
    }  
  if (main_pres_ev == 1) {  
    main_pres_ev = 2;  
    }  
  else {  
    }  
  if (main_dbl_ev == 1) {  
    main_dbl_ev = 2;  
    }  
  else {  
    }  
  if (main_zero_ev == 1) {  
    main_zero_ev = 2;  
    }  
  else {  
    }  
  if (main_clk_ev == 1) {  
    main_clk_ev = 2;  
    }  
  else {  
    }  
  if (main_clk_pos_edge == 1) {  
    main_clk_pos_edge = 2;  
    }  
  else {  
    }  
  if (main_clk_neg_edge == 1) {  
    main_clk_neg_edge = 2;  
    }  
  else {  
    }  
  {  
    while (1) {  
      {  
        while_1_continue: ;  
        {  
          kernel_st = 1;  
                    eval();  
          }  
        kernel_st = 2;  
        if (main_in1_req_up == 1) {  
          if (main_in1_val != main_in1_val_t) {  
            main_in1_val = main_in1_val_t;  
            main_in1_ev = 0;  
            }  
          else {  
            }  
          main_in1_req_up = 0;  
          }  
        else {  
          }  
        if (main_in2_req_up == 1) {  
          if (main_in2_val != main_in2_val_t) {  
            main_in2_val = main_in2_val_t;  
            main_in2_ev = 0;  
            }  
          else {  
            }  
          main_in2_req_up = 0;  
          }  
        else {  
          }  
        if (main_sum_req_up == 1) {  
          if (main_sum_val != main_sum_val_t) {  
            main_sum_val = main_sum_val_t;  
            main_sum_ev = 0;  
            }  
          else {  
            }  
          main_sum_req_up = 0;  
          }  
        else {  
          }  
        if (main_diff_req_up == 1) {  
          if (main_diff_val != main_diff_val_t) {  
            main_diff_val = main_diff_val_t;  
            main_diff_ev = 0;  
            }  
          else {  
            }  
          main_diff_req_up = 0;  
          }  
        else {  
          }  
        if (main_pres_req_up == 1) {  
          if (main_pres_val != main_pres_val_t) {  
            main_pres_val = main_pres_val_t;  
            main_pres_ev = 0;  
            }  
          else {  
            }  
          main_pres_req_up = 0;  
          }  
        else {  
          }  
        if (main_dbl_req_up == 1) {  
          if (main_dbl_val != main_dbl_val_t) {  
            main_dbl_val = main_dbl_val_t;  
            main_dbl_ev = 0;  
            }  
          else {  
            }  
          main_dbl_req_up = 0;  
          }  
        else {  
          }  
        if (main_zero_req_up == 1) {  
          if (main_zero_val != main_zero_val_t) {  
            main_zero_val = main_zero_val_t;  
            main_zero_ev = 0;  
            }  
          else {  
            }  
          main_zero_req_up = 0;  
          }  
        else {  
          }  
        if (main_clk_req_up == 1) {  
          if (main_clk_val != main_clk_val_t) {  
            main_clk_val = main_clk_val_t;  
            main_clk_ev = 0;  
            if (main_clk_val == 1) {  
              main_clk_pos_edge = 0;  
              main_clk_neg_edge = 2;  
              }  
            else {  
              main_clk_neg_edge = 0;  
              main_clk_pos_edge = 2;  
              }  
            }  
          else {  
            }  
          main_clk_req_up = 0;  
          }  
        else {  
          }  
        kernel_st = 3;  
        if (main_in1_ev == 0) {  
          main_in1_ev = 1;  
          }  
        else {  
          }  
        if (main_in2_ev == 0) {  
          main_in2_ev = 1;  
          }  
        else {  
          }  
        if (main_sum_ev == 0) {  
          main_sum_ev = 1;  
          }  
        else {  
          }  
        if (main_diff_ev == 0) {  
          main_diff_ev = 1;  
          }  
        else {  
          }  
        if (main_pres_ev == 0) {  
          main_pres_ev = 1;  
          }  
        else {  
          }  
        if (main_dbl_ev == 0) {  
          main_dbl_ev = 1;  
          }  
        else {  
          }  
        if (main_zero_ev == 0) {  
          main_zero_ev = 1;  
          }  
        else {  
          }  
        if (main_clk_ev == 0) {  
          main_clk_ev = 1;  
          }  
        else {  
          }  
        if (main_clk_pos_edge == 0) {  
          main_clk_pos_edge = 1;  
          }  
        else {  
          }  
        if (main_clk_neg_edge == 0) {  
          main_clk_neg_edge = 1;  
          }  
        else {  
          }  
        if (main_clk_pos_edge == 1) {  
          N_generate_st = 0;  
          }  
        else {  
          }  
        if (main_clk_pos_edge == 1) {  
          S1_addsub_st = 0;  
          }  
        else {  
          }  
        if (main_clk_pos_edge == 1) {  
          S2_presdbl_st = 0;  
          }  
        else {  
          }  
        if (main_clk_pos_edge == 1) {  
          S3_zero_st = 0;  
          }  
        else {  
          }  
        if (main_clk_pos_edge == 1) {  
          D_print_st = 0;  
          }  
        else {  
          }  
        if (main_in1_ev == 1) {  
          main_in1_ev = 2;  
          }  
        else {  
          }  
        if (main_in2_ev == 1) {  
          main_in2_ev = 2;  
          }  
        else {  
          }  
        if (main_sum_ev == 1) {  
          main_sum_ev = 2;  
          }  
        else {  
          }  
        if (main_diff_ev == 1) {  
          main_diff_ev = 2;  
          }  
        else {  
          }  
        if (main_pres_ev == 1) {  
          main_pres_ev = 2;  
          }  
        else {  
          }  
        if (main_dbl_ev == 1) {  
          main_dbl_ev = 2;  
          }  
        else {  
          }  
        if (main_zero_ev == 1) {  
          main_zero_ev = 2;  
          }  
        else {  
          }  
        if (main_clk_ev == 1) {  
          main_clk_ev = 2;  
          }  
        else {  
          }  
        if (main_clk_pos_edge == 1) {  
          main_clk_pos_edge = 2;  
          }  
        else {  
          }  
        if (main_clk_neg_edge == 1) {  
          main_clk_neg_edge = 2;  
          }  
        else {  
          }  
        if (N_generate_st == 0) {  
          }  
        else {  
          if (S1_addsub_st == 0) {  
            }  
          else {  
            if (S2_presdbl_st == 0) {  
              }  
            else {  
              if (S3_zero_st == 0) {  
                }  
              else {  
                if (D_print_st == 0) {  
                  }  
                else {  
                  goto while_1_break;  
                  }  
                }  
              }  
            }  
          }  
        }  
      }  
    while_1_break: ;  
    }  
  return;  
  }  
}  
  
void main () {  
//  
// Number of lvals: 62  
//   Frama_C_interval: int (int min, int max)  
//      int (int min, int max)  
//   error: void (void)  
//      void (void)  
//   count: int  
//      int  
//   res: int  
//      int  
//   modFlag: int  
//      int  
//   main_in1_val: int  
//      int  
//   main_in1_val_t: int  
//      int  
//   main_in1_ev: int  
//      int  
//   main_in1_req_up: int  
//      int  
//   main_in2_val: int  
//      int  
//   main_in2_val_t: int  
//      int  
//   main_in2_ev: int  
//      int  
//   main_in2_req_up: int  
//      int  
//   main_diff_val: int  
//      int  
//   main_diff_val_t: int  
//      int  
//   main_diff_ev: int  
//      int  
//   main_diff_req_up: int  
//      int  
//   main_sum_val: int  
//      int  
//   main_sum_val_t: int  
//      int  
//   main_sum_ev: int  
//      int  
//   main_sum_req_up: int  
//      int  
//   main_pres_val: int  
//      int  
//   main_pres_val_t: int  
//      int  
//   main_pres_ev: int  
//      int  
//   main_pres_req_up: int  
//      int  
//   main_dbl_val: int  
//      int  
//   main_dbl_val_t: int  
//      int  
//   main_dbl_ev: int  
//      int  
//   main_dbl_req_up: int  
//      int  
//   main_zero_val: int  
//      int  
//   main_zero_val_t: int  
//      int  
//   main_zero_ev: int  
//      int  
//   main_zero_req_up: int  
//      int  
//   main_clk_val: int  
//      int  
//   main_clk_val_t: int  
//      int  
//   main_clk_ev: int  
//      int  
//   main_clk_req_up: int  
//      int  
//   main_clk_pos_edge: int  
//      int  
//   main_clk_neg_edge: int  
//      int  
//   N_generate_st: int  
//      int  
//   N_generate_i: int  
//      int  
//   S1_addsub_st: int  
//      int  
//   S1_addsub_i: int  
//      int  
//   S2_presdbl_st: int  
//      int  
//   S2_presdbl_i: int  
//      int  
//   S3_zero_st: int  
//      int  
//   S3_zero_i: int  
//      int  
//   D_z: int  
//      int  
//   D_print_st: int  
//      int  
//   D_print_i: int  
//      int  
//   N_generate: void (void)  
//      void (void)  
//   S1_addsub: void (void)  
//      void (void)  
//   S2_presdbl: void (void)  
//      void (void)  
//   S3_zero: void (void)  
//      void (void)  
//   D_print: void (void)  
//      void (void)  
//   eval: void (void)  
//      void (void)  
//   start_simulation: void (void)  
//      void (void)  
//   n1: int  
//      int  
//   n2: int  
//      int  
//   n3: int  
//      int  
//   bound: int  
//      int  
//   i: int  
//      int  
//  
  
D_print_i = __VERIFIER_nondet_int();  
D_print_st = __VERIFIER_nondet_int();  
D_z = __VERIFIER_nondet_int();  
N_generate_i = __VERIFIER_nondet_int();  
N_generate_st = __VERIFIER_nondet_int();  
S1_addsub_i = __VERIFIER_nondet_int();  
S1_addsub_st = __VERIFIER_nondet_int();  
S2_presdbl_i = __VERIFIER_nondet_int();  
S2_presdbl_st = __VERIFIER_nondet_int();  
S3_zero_i = __VERIFIER_nondet_int();  
S3_zero_st = __VERIFIER_nondet_int();  
count = __VERIFIER_nondet_int();  
main_clk_ev = __VERIFIER_nondet_int();  
main_clk_neg_edge = __VERIFIER_nondet_int();  
main_clk_pos_edge = __VERIFIER_nondet_int();  
main_clk_req_up = __VERIFIER_nondet_int();  
main_clk_val = __VERIFIER_nondet_int();  
main_clk_val_t = __VERIFIER_nondet_int();  
main_dbl_ev = __VERIFIER_nondet_int();  
main_dbl_req_up = __VERIFIER_nondet_int();  
main_dbl_val = __VERIFIER_nondet_int();  
main_dbl_val_t = __VERIFIER_nondet_int();  
main_diff_ev = __VERIFIER_nondet_int();  
main_diff_req_up = __VERIFIER_nondet_int();  
main_diff_val = __VERIFIER_nondet_int();  
main_diff_val_t = __VERIFIER_nondet_int();  
main_in1_ev = __VERIFIER_nondet_int();  
main_in1_req_up = __VERIFIER_nondet_int();  
main_in1_val = __VERIFIER_nondet_int();  
main_in1_val_t = __VERIFIER_nondet_int();  
main_in2_ev = __VERIFIER_nondet_int();  
main_in2_req_up = __VERIFIER_nondet_int();  
main_in2_val = __VERIFIER_nondet_int();  
main_in2_val_t = __VERIFIER_nondet_int();  
main_pres_ev = __VERIFIER_nondet_int();  
main_pres_req_up = __VERIFIER_nondet_int();  
main_pres_val = __VERIFIER_nondet_int();  
main_pres_val_t = __VERIFIER_nondet_int();  
main_sum_ev = __VERIFIER_nondet_int();  
main_sum_req_up = __VERIFIER_nondet_int();  
main_sum_val = __VERIFIER_nondet_int();  
main_sum_val_t = __VERIFIER_nondet_int();  
main_zero_ev = __VERIFIER_nondet_int();  
main_zero_req_up = __VERIFIER_nondet_int();  
main_zero_val = __VERIFIER_nondet_int();  
main_zero_val_t = __VERIFIER_nondet_int();  
modFlag = __VERIFIER_nondet_int();  
res = __VERIFIER_nondet_int();  
  
  
  
{  
  int n1 = 3;  
  int n2 = 5;  
  int n3 = 7;  
  res = 0;  
  auto int bound;  
  bound = __VERIFIER_nondet_int();  
  {  
    int i = 0;  
    while (1) {  
      if (i < bound) {  
        }  
      else {  
        break;  
        }  
      {  
        if (i % n1 == 0) {  
          if (i % n2 == 0) {  
            if (i % n3 == 0) {  
              res = i;  
              }  
            else {  
              }  
            }  
          else {  
            }  
          }  
        else {  
          }  
        }  
      i ++;  
      }  
    }  
  {  
    modFlag = res;  
    }  
  if (modFlag % 105 == 0) {  
    {  
      count = 0;  
      main_in1_ev = 2;  
      main_in1_req_up = 0;  
      main_in2_ev = 2;  
      main_in2_req_up = 0;  
      main_diff_ev = 2;  
      main_diff_req_up = 0;  
      main_sum_ev = 2;  
      main_sum_req_up = 0;  
      main_pres_ev = 2;  
      main_pres_req_up = 0;  
      main_dbl_ev = 2;  
      main_dbl_req_up = 0;  
      main_zero_ev = 2;  
      main_zero_req_up = 0;  
      main_clk_val = 0;  
      main_clk_ev = 2;  
      main_clk_req_up = 0;  
      main_clk_pos_edge = 2;  
      main_clk_neg_edge = 2;  
      count = 0;  
      N_generate_i = 0;  
      S1_addsub_i = 0;  
      S2_presdbl_i = 0;  
      S3_zero_i = 0;  
      D_print_i = 0;  
            start_simulation();  
      }  
    {  
      while (1) {  
        {  
          while_2_continue: ;  
          {  
            main_clk_val_t = 1;  
            main_clk_req_up = 1;  
                        start_simulation();  
            count ++;  
            }  
          if (count == 5) {  
            if (! (D_z == 0)) {  
                            error();  
              }  
            else {  
              }  
            count = 0;  
            }  
          else {  
            }  
          {  
            main_clk_val_t = 0;  
            main_clk_req_up = 1;  
                        start_simulation();  
            }  
          }  
        }  
      }  
    }  
  else {  
        error();  
    }  
  }  
return;  
}  

DateTimeLevelComponentMessage
2023-06-2804:19:09:396INFOCPAMain.detectFrontendLanguageIfNecessaryLanguage C detected and set for analysis
2023-06-2804:19:09:413INFOResourceLimitChecker.fromConfigurationUsing the following resource limits: CPU-time limit of 900s
2023-06-2804:19:09:467INFOCPAchecker.runCPAchecker 2.2 / svcomp23 (OpenJDK 64-Bit Server VM 11.0.19) started
2023-06-2804:19:09:484INFOCPAchecker.parseParsing CFA from file(s) "no_context/combo2.c"
2023-06-2804:19:10:457INFOCoreComponentsFactory.createAlgorithmUsing heuristics to select analysis
2023-06-2804:19:10:469WARNINGCPAchecker.printConfigurationWarningsThe following configuration options were specified but are not used:
 cpa.callstack.unsupportedFunctions
 termination.violation.witness
 cpa.predicate.memoryAllocationsAlwaysSucceed
 cpa.arg.compressWitness
 cpa.callstack.skipFunctionPointerRecursion
 cpa.composite.aggregateBasicBlocks
 counterexample.export.graphml
 counterexample.export.compressWitness
 cpa.arg.proofWitness 
2023-06-2804:19:10:469INFOCPAchecker.runAlgorithmStarting analysis ...
2023-06-2804:19:10:473INFOSelectionAlgorithm.chooseConfigPerforming heuristic ...
2023-06-2804:19:10:477INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
ResourceLimitChecker.fromConfigurationUsing the following resource limits: CPU-time limit of 900s
2023-06-2804:19:10:502INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
CoreComponentsFactory.createAlgorithmUsing Restarting Algorithm
2023-06-2804:19:10:508INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
RestartAlgorithm.runLoading analysis 1 from file /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-symbolicExecution.properties ...
2023-06-2804:19:10:513INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
NestingAlgorithm.checkConfigsMismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-symbolicExecution.properties': 'cpa.composite.aggregateBasicBlocks' has two values 'false' and 'true'. Using 'true'.
2023-06-2804:19:10:513INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
NestingAlgorithm.checkConfigsMismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-symbolicExecution.properties': 'limits.time.cpu' has two values '900s' and '140s'. Using '140s'.
2023-06-2804:19:10:513INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
NestingAlgorithm.checkConfigsMismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-symbolicExecution.properties': 'limits.time.cpu::required' has two values '900' and '140s'. Using '140s'.
2023-06-2804:19:10:514INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-symbolicExecution.properties
ResourceLimitChecker.fromConfigurationUsing the following resource limits: CPU-time limit of 140s
2023-06-2804:19:10:809INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
RestartAlgorithm.runStarting analysis 1 ...
2023-06-2804:21:12:614WARNINGAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
ShutdownNotifier.shutdownIfNecessaryWarning: Analysis 1 stopped. (The CPU-time limit of 140s has elapsed.)
2023-06-2804:21:12:956INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
RestartAlgorithm.runRestartAlgorithm switches to the next configuration...
2023-06-2804:21:12:957INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
RestartAlgorithm.runLoading analysis 2 from file /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-valueAnalysis-Cegar.properties ...
2023-06-2804:21:12:960INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
NestingAlgorithm.checkConfigsMismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-valueAnalysis-Cegar.properties': 'cpa.composite.aggregateBasicBlocks' has two values 'false' and 'true'. Using 'true'.
2023-06-2804:21:12:960INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
NestingAlgorithm.checkConfigsMismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-valueAnalysis-Cegar.properties': 'limits.time.cpu' has two values '900s' and '60s'. Using '60s'.
2023-06-2804:21:12:961INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
NestingAlgorithm.checkConfigsMismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-valueAnalysis-Cegar.properties': 'limits.time.cpu::required' has two values '900' and '60s'. Using '60s'.
2023-06-2804:21:12:961INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-valueAnalysis-Cegar.properties
ResourceLimitChecker.fromConfigurationUsing the following resource limits: CPU-time limit of 60s
2023-06-2804:21:13:014INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
RestartAlgorithm.runStarting analysis 2 ...
2023-06-2804:21:13:104INFOCPAchecker.runAlgorithmStopping analysis ...

        

Date	Time	Level	Component	Message
2023-06-28	04:19:09:396	INFO	CPAMain.detectFrontendLanguageIfNecessary	Language C detected and set for analysis
2023-06-28	04:19:09:413	INFO	ResourceLimitChecker.fromConfiguration	Using the following resource limits: CPU-time limit of 900s
2023-06-28	04:19:09:467	INFO	CPAchecker.run	CPAchecker 2.2 / svcomp23 (OpenJDK 64-Bit Server VM 11.0.19) started
2023-06-28	04:19:09:484	INFO	CPAchecker.parse	Parsing CFA from file(s) "no_context/combo2.c"
2023-06-28	04:19:10:457	INFO	CoreComponentsFactory.createAlgorithm	Using heuristics to select analysis
2023-06-28	04:19:10:469	WARNING	CPAchecker.printConfigurationWarnings	The following configuration options were specified but are not used: cpa.callstack.unsupportedFunctions termination.violation.witness cpa.predicate.memoryAllocationsAlwaysSucceed cpa.arg.compressWitness cpa.callstack.skipFunctionPointerRecursion cpa.composite.aggregateBasicBlocks counterexample.export.graphml counterexample.export.compressWitness cpa.arg.proofWitness
2023-06-28	04:19:10:469	INFO	CPAchecker.runAlgorithm	Starting analysis ...
2023-06-28	04:19:10:473	INFO	SelectionAlgorithm.chooseConfig	Performing heuristic ...
2023-06-28	04:19:10:477	INFO	Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties ResourceLimitChecker.fromConfiguration	Using the following resource limits: CPU-time limit of 900s
2023-06-28	04:19:10:502	INFO	Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties CoreComponentsFactory.createAlgorithm	Using Restarting Algorithm
2023-06-28	04:19:10:508	INFO	Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties RestartAlgorithm.run	Loading analysis 1 from file /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-symbolicExecution.properties ...
2023-06-28	04:19:10:513	INFO	Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties NestingAlgorithm.checkConfigs	Mismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-symbolicExecution.properties': 'cpa.composite.aggregateBasicBlocks' has two values 'false' and 'true'. Using 'true'.
2023-06-28	04:19:10:513	INFO	Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties NestingAlgorithm.checkConfigs	Mismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-symbolicExecution.properties': 'limits.time.cpu' has two values '900s' and '140s'. Using '140s'.
2023-06-28	04:19:10:513	INFO	Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties NestingAlgorithm.checkConfigs	Mismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-symbolicExecution.properties': 'limits.time.cpu::required' has two values '900' and '140s'. Using '140s'.
2023-06-28	04:19:10:514	INFO	Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-symbolicExecution.properties ResourceLimitChecker.fromConfiguration	Using the following resource limits: CPU-time limit of 140s
2023-06-28	04:19:10:809	INFO	Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties RestartAlgorithm.run	Starting analysis 1 ...
2023-06-28	04:21:12:614	WARNING	Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties ShutdownNotifier.shutdownIfNecessary	Warning: Analysis 1 stopped. (The CPU-time limit of 140s has elapsed.)
2023-06-28	04:21:12:956	INFO	Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties RestartAlgorithm.run	RestartAlgorithm switches to the next configuration...
2023-06-28	04:21:12:957	INFO	Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties RestartAlgorithm.run	Loading analysis 2 from file /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-valueAnalysis-Cegar.properties ...
2023-06-28	04:21:12:960	INFO	Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties NestingAlgorithm.checkConfigs	Mismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-valueAnalysis-Cegar.properties': 'cpa.composite.aggregateBasicBlocks' has two values 'false' and 'true'. Using 'true'.
2023-06-28	04:21:12:960	INFO	Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties NestingAlgorithm.checkConfigs	Mismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-valueAnalysis-Cegar.properties': 'limits.time.cpu' has two values '900s' and '60s'. Using '60s'.
2023-06-28	04:21:12:961	INFO	Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties NestingAlgorithm.checkConfigs	Mismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-valueAnalysis-Cegar.properties': 'limits.time.cpu::required' has two values '900' and '60s'. Using '60s'.
2023-06-28	04:21:12:961	INFO	Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-valueAnalysis-Cegar.properties ResourceLimitChecker.fromConfiguration	Using the following resource limits: CPU-time limit of 60s
2023-06-28	04:21:13:014	INFO	Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties RestartAlgorithm.run	Starting analysis 2 ...
2023-06-28	04:21:13:104	INFO	CPAchecker.runAlgorithm	Stopping analysis ...

Statistics NameStatistics ValueAdditional Value
Selection Algorithm statistics
Size of preliminary analysis reached set      0
Used algorithm property                       /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
Program containing only relevant bools        0
Relevant boolean vars / relevant vars ratio   0.0676
Requires alias handling                       0
Requires loop handling                        1
Has a single loop                             0
Requires composite-type handling              0
Requires array handling                       0
Requires float handling                       0
Requires recursion handling                   0
Relevant addressed vars / relevant vars ratio 0.0000
Program containing external functions         true
Number of all righthand side functions        9
Restart Algorithm statistics
Number of algorithms provided    7
Number of algorithms used        2
Total time for algorithm 2     0.147s
ValueAnalysisCPA statistics
Number of variables per state                     0.00 sum: 0, count: 1448, min: 0, max: 0
Number of global variables per state              0.00 sum: 0, count: 1448, min: 0, max: 0
Number of assumptions                                  668
Number of deterministic assumptions                      0
Level of Determinism                              0%
ValueAnalysisPrecisionAdjustment statistics
Number of abstraction computations                    1781
Total time for liveness abstraction                   0.000s
Total time for abstraction computation                0.007s
Total time for path thresholds                        0.000s
ConstraintsStrengthenOperator statistics
Total time for strengthening by ConstraintsCPA     0.000s
Replaced symbolic expressions 0
AutomatonAnalysis (SVCOMP) statistics
Number of states                                  1
Total time for successor computation                  0.001s
Automaton transfers with branching                0
Automaton transfer successors                     1.00 sum: 2122, count: 2122, min: 1, max: 1 [1 x 2122]
Number of states with assumption transitions      0
CPA algorithm statistics
Number of iterations            1448
Max size of waitlist            27
Average size of waitlist        13
Number of computed successors   1781
Max successors for one state    2
Number of times merged          0
Number of times stopped         334
Number of times breaked         0
Total time for CPA algorithm         0.079s Max:     0.079s
	  Time for choose from waitlist      0.012s
	  Time for precision adjustment      0.014s
	  Time for transfer relation         0.029s
	  Time for stop operator             0.004s
	  Time for adding to reached set     0.010s
ValueAnalysisRefiner statistics
Number of refinements                                    0
Number of targets found                                  0 count: 0, min: 0, max: 0, avg: 0.00
Time for completing refinement                        0.000s
Number of root relocations                               0
Number of similar, repeated refinements                  0
Number of unique precision increments             0
PathExtractor statistics
Total number of targets found            0
ValueAnalysisPathInterpolator statistics
	  Time for interpolation                              0.000s
	  Number of interpolations                               0
	  Number of interpolation queries                        0 count: 0, min: 0, max: 0, avg: 0.00
	  Size of interpolant                             0.00 sum: 0, count: 0, min: 0, max: 0
	  Number of sliced prefixes                              0 count: 0, min: 0, max: 0, avg: 0.00
	  Extracting infeasible sliced prefixes               0.000s
	  Selecting infeasible sliced prefixes                0.000s
CEGAR algorithm statistics
Number of CEGAR refinements          0
Counterexample-Check Algorithm statistics
Number of counterexample checks    0
CPA algorithm statistics
Number of iterations            1448
Max size of waitlist            27
Average size of waitlist        13
Number of computed successors   1781
Max successors for one state    2
Number of times merged          0
Number of times stopped         334
Number of times breaked         0
Total time for CPA algorithm         0.079s Max:     0.079s
	  Time for choose from waitlist      0.012s
	  Time for precision adjustment      0.014s
	  Time for transfer relation         0.029s
	  Time for stop operator             0.004s
	  Time for adding to reached set     0.010s
ValueAnalysisRefiner statistics
Number of refinements                                    0
Number of targets found                                  0 count: 0, min: 0, max: 0, avg: 0.00
Time for completing refinement                        0.000s
Number of root relocations                               0
Number of similar, repeated refinements                  0
Number of unique precision increments             0
PathExtractor statistics
Total number of targets found            0
ValueAnalysisPathInterpolator statistics
	  Time for interpolation                              0.000s
	  Number of interpolations                               0
	  Number of interpolation queries                        0 count: 0, min: 0, max: 0, avg: 0.00
	  Size of interpolant                             0.00 sum: 0, count: 0, min: 0, max: 0
	  Number of sliced prefixes                              0 count: 0, min: 0, max: 0, avg: 0.00
	  Extracting infeasible sliced prefixes               0.000s
	  Selecting infeasible sliced prefixes                0.000s
CEGAR algorithm statistics
Number of CEGAR refinements          0
Counterexample-Check Algorithm statistics
Number of counterexample checks    0
Code Coverage
	  Function coverage      1.000
	  Visited lines          457
	  Total lines            457
	  Line coverage          1.000
	  Visited conditions     232
	  Total conditions       232
	  Condition coverage     1.000
CPAchecker general statistics
Number of program locations                       734
Number of CFA edges (per node)                         863 count: 734, min: 0, max: 3, avg: 1.18
Number of relevant variables                      74
Number of functions                               9
Number of loops (and loop nodes)                         4 sum: 291, min: 17, max: 196, avg: 72.75
Size of reached set             1448
	  Number of reached locations   513 70%
		    Avg states per location     2
		    Max states per location     3 at node N7
	  Number of reached functions   9 100%
	  Number of target states       0
Time for analysis setup          0.985s
	  Time for loading CPAs          0.134s
	  Time for loading parser        0.146s
	  Time for CFA construction      0.678s
		    Time for parsing file(s)     0.258s
		    Time for AST to CFA          0.160s
		    Time for CFA sanity check    0.046s
		    Time for post-processing     0.150s
		    Time for CFA export          0.849s
			      Time for function pointers resolving            0.005s
				        Function calls via function pointers             0 count: 1, min: 0, max: 0, avg: 0.00
				        Instrumented function pointer calls              0 count: 1, min: 0, max: 0, avg: 0.00
				        Function calls with function pointer arguments        0 count: 1, min: 0, max: 0, avg: 0.00
				        Instrumented function pointer arguments          0 count: 1, min: 0, max: 0, avg: 0.00
			      Time for classifying variables                  0.086s
				        Time for collecting variables                 0.030s
				        Time for solving dependencies                 0.001s
				        Time for building hierarchy                   0.000s
				        Time for building classification              0.050s
				        Time for exporting data                       0.005s
Time for Analysis              122.635s
CPU time for analysis          141.270s
Time for analyzing result        0.001s
Total time for CPAchecker      123.621s
Total CPU time for CPAchecker  144.150s
Time for statistics              0.054s
Time for Garbage Collector       1.302s in 57 runs
Garbage Collector(s) used    G1 Old Generation, G1 Young Generation
Used heap memory                674MB (   643 MiB) max;    323MB (   308 MiB) avg;    693MB (   660 MiB) peak
Used non-heap memory             54MB (    51 MiB) max;     52MB (    49 MiB) avg;     55MB (    52 MiB) peak
Used in G1 Old Gen pool         163MB (   155 MiB) max;     97MB (    93 MiB) avg;    163MB (   155 MiB) peak
Allocated heap memory           871MB (   831 MiB) max;    721MB (   688 MiB) avg
Allocated non-heap memory        57MB (    54 MiB) max;     54MB (    52 MiB) avg
Total process virtual memory  12222MB ( 11656 MiB) max;  12217MB ( 11651 MiB) avg

        

Statistics Name	Statistics Value	Additional Value
Selection Algorithm statistics
Size of preliminary analysis reached set	0
Used algorithm property	/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
Program containing only relevant bools	0
Relevant boolean vars / relevant vars ratio	0.0676
Requires alias handling	0
Requires loop handling	1
Has a single loop	0
Requires composite-type handling	0
Requires array handling	0
Requires float handling	0
Requires recursion handling	0
Relevant addressed vars / relevant vars ratio	0.0000
Program containing external functions	true
Number of all righthand side functions	9
Restart Algorithm statistics
Number of algorithms provided	7
Number of algorithms used	2
Total time for algorithm 2	0.147s
ValueAnalysisCPA statistics
Number of variables per state	0.00	sum: 0, count: 1448, min: 0, max: 0
Number of global variables per state	0.00	sum: 0, count: 1448, min: 0, max: 0
Number of assumptions	668
Number of deterministic assumptions	0
Level of Determinism	0%
ValueAnalysisPrecisionAdjustment statistics
Number of abstraction computations	1781
Total time for liveness abstraction	0.000s
Total time for abstraction computation	0.007s
Total time for path thresholds	0.000s
ConstraintsStrengthenOperator statistics
Total time for strengthening by ConstraintsCPA	0.000s
Replaced symbolic expressions	0
AutomatonAnalysis (SVCOMP) statistics
Number of states	1
Total time for successor computation	0.001s
Automaton transfers with branching	0
Automaton transfer successors	1.00	sum: 2122, count: 2122, min: 1, max: 1 [1 x 2122]
Number of states with assumption transitions	0
CPA algorithm statistics
Number of iterations	1448
Max size of waitlist	27
Average size of waitlist	13
Number of computed successors	1781
Max successors for one state	2
Number of times merged	0
Number of times stopped	334
Number of times breaked	0
Total time for CPA algorithm	0.079s	Max: 0.079s
Time for choose from waitlist	0.012s
Time for precision adjustment	0.014s
Time for transfer relation	0.029s
Time for stop operator	0.004s
Time for adding to reached set	0.010s
ValueAnalysisRefiner statistics
Number of refinements	0
Number of targets found	0	count: 0, min: 0, max: 0, avg: 0.00
Time for completing refinement	0.000s
Number of root relocations	0
Number of similar, repeated refinements	0
Number of unique precision increments	0
PathExtractor statistics
Total number of targets found	0
ValueAnalysisPathInterpolator statistics
Time for interpolation	0.000s
Number of interpolations	0
Number of interpolation queries	0	count: 0, min: 0, max: 0, avg: 0.00
Size of interpolant	0.00	sum: 0, count: 0, min: 0, max: 0
Number of sliced prefixes	0	count: 0, min: 0, max: 0, avg: 0.00
Extracting infeasible sliced prefixes	0.000s
Selecting infeasible sliced prefixes	0.000s
CEGAR algorithm statistics
Number of CEGAR refinements	0
Counterexample-Check Algorithm statistics
Number of counterexample checks	0
CPA algorithm statistics
Number of iterations	1448
Max size of waitlist	27
Average size of waitlist	13
Number of computed successors	1781
Max successors for one state	2
Number of times merged	0
Number of times stopped	334
Number of times breaked	0
Total time for CPA algorithm	0.079s	Max: 0.079s
Time for choose from waitlist	0.012s
Time for precision adjustment	0.014s
Time for transfer relation	0.029s
Time for stop operator	0.004s
Time for adding to reached set	0.010s
ValueAnalysisRefiner statistics
Number of refinements	0
Number of targets found	0	count: 0, min: 0, max: 0, avg: 0.00
Time for completing refinement	0.000s
Number of root relocations	0
Number of similar, repeated refinements	0
Number of unique precision increments	0
PathExtractor statistics
Total number of targets found	0
ValueAnalysisPathInterpolator statistics
Time for interpolation	0.000s
Number of interpolations	0
Number of interpolation queries	0	count: 0, min: 0, max: 0, avg: 0.00
Size of interpolant	0.00	sum: 0, count: 0, min: 0, max: 0
Number of sliced prefixes	0	count: 0, min: 0, max: 0, avg: 0.00
Extracting infeasible sliced prefixes	0.000s
Selecting infeasible sliced prefixes	0.000s
CEGAR algorithm statistics
Number of CEGAR refinements	0
Counterexample-Check Algorithm statistics
Number of counterexample checks	0
Code Coverage
Function coverage	1.000
Visited lines	457
Total lines	457
Line coverage	1.000
Visited conditions	232
Total conditions	232
Condition coverage	1.000
CPAchecker general statistics
Number of program locations	734
Number of CFA edges (per node)	863	count: 734, min: 0, max: 3, avg: 1.18
Number of relevant variables	74
Number of functions	9
Number of loops (and loop nodes)	4	sum: 291, min: 17, max: 196, avg: 72.75
Size of reached set	1448
Number of reached locations	513	70%
Avg states per location	2
Max states per location	3	at node N7
Number of reached functions	9	100%
Number of target states	0
Time for analysis setup	0.985s
Time for loading CPAs	0.134s
Time for loading parser	0.146s
Time for CFA construction	0.678s
Time for parsing file(s)	0.258s
Time for AST to CFA	0.160s
Time for CFA sanity check	0.046s
Time for post-processing	0.150s
Time for CFA export	0.849s
Time for function pointers resolving	0.005s
Function calls via function pointers	0	count: 1, min: 0, max: 0, avg: 0.00
Instrumented function pointer calls	0	count: 1, min: 0, max: 0, avg: 0.00
Function calls with function pointer arguments	0	count: 1, min: 0, max: 0, avg: 0.00
Instrumented function pointer arguments	0	count: 1, min: 0, max: 0, avg: 0.00
Time for classifying variables	0.086s
Time for collecting variables	0.030s
Time for solving dependencies	0.001s
Time for building hierarchy	0.000s
Time for building classification	0.050s
Time for exporting data	0.005s
Time for Analysis	122.635s
CPU time for analysis	141.270s
Time for analyzing result	0.001s
Total time for CPAchecker	123.621s
Total CPU time for CPAchecker	144.150s
Time for statistics	0.054s
Time for Garbage Collector	1.302s	in 57 runs
Garbage Collector(s) used	G1 Old Generation, G1 Young Generation
Used heap memory	674MB ( 643 MiB) max; 323MB ( 308 MiB) avg; 693MB ( 660 MiB) peak
Used non-heap memory	54MB ( 51 MiB) max; 52MB ( 49 MiB) avg; 55MB ( 52 MiB) peak
Used in G1 Old Gen pool	163MB ( 155 MiB) max; 97MB ( 93 MiB) avg; 163MB ( 155 MiB) peak
Allocated heap memory	871MB ( 831 MiB) max; 721MB ( 688 MiB) avg
Allocated non-heap memory	57MB ( 54 MiB) max; 54MB ( 52 MiB) avg
Total process virtual memory	12222MB ( 11656 MiB) max; 12217MB ( 11651 MiB) avg

#Configuration NameConfiguration Value
1analysis.entryFunction  main
2analysis.name  svcomp23
3analysis.programNames  no_context/combo2.c
4analysis.selectAnalysisHeuristically  true
5analysis.summaryEdges  true
6cfa.simplifyCfa  false
7cfa.useCFACloningForMultiThreadedPrograms  true
8counterexample.export.compressWitness  false
9counterexample.export.graphml  witness.graphml
10cpa.arg.compressWitness  false
11cpa.arg.proofWitness  witness.graphml
12cpa.callstack.skipFunctionPointerRecursion  true
13cpa.callstack.unsupportedFunctions  pthread_create,pthread_key_create,sin,cos,__builtin_uaddl_overflow
14cpa.composite.aggregateBasicBlocks  false
15cpa.predicate.memoryAllocationsAlwaysSucceed  true
16datarace.config  svcomp23--datarace.properties
17heuristicSelection.addressedRatio  0.0
18heuristicSelection.complexLoopConfig  components/svcomp23--configselection-restart-valueAnalysis-fallbacks.properties
19heuristicSelection.loopConfig  components/svcomp23--multipleLoopsConfig.properties
20heuristicSelection.loopFreeConfig  components/svcomp23--configselection-restart-bmc-fallbacks.properties
21heuristicSelection.singleLoopConfig  components/svcomp23--singleLoopConfig.properties
22language  C
23limits.time.cpu  900s
24limits.time.cpu::required  900
25log.level  INFO
26memorycleanup.config  svcomp23--memorycleanup.properties
27memorysafety.config  svcomp23--memorysafety.properties
28overflow.config  svcomp23--overflow.properties
29parser.usePreprocessor  true
30specification  /home/artjom/CPAchecker-2.2-unix/config/properties/unreach-call.prp
31statistics.print  true
32termination.config  svcomp23--termination.properties
33termination.violation.witness  witness.graphml

        

#	Configuration Name	Configuration Value
1	analysis.entryFunction	main
2	analysis.name	svcomp23
3	analysis.programNames	no_context/combo2.c
4	analysis.selectAnalysisHeuristically	true
5	analysis.summaryEdges	true
6	cfa.simplifyCfa	false
7	cfa.useCFACloningForMultiThreadedPrograms	true
8	counterexample.export.compressWitness	false
9	counterexample.export.graphml	witness.graphml
10	cpa.arg.compressWitness	false
11	cpa.arg.proofWitness	witness.graphml
12	cpa.callstack.skipFunctionPointerRecursion	true
13	cpa.callstack.unsupportedFunctions	pthread_create,pthread_key_create,sin,cos,__builtin_uaddl_overflow
14	cpa.composite.aggregateBasicBlocks	false
15	cpa.predicate.memoryAllocationsAlwaysSucceed	true
16	datarace.config	svcomp23--datarace.properties
17	heuristicSelection.addressedRatio	0.0
18	heuristicSelection.complexLoopConfig	components/svcomp23--configselection-restart-valueAnalysis-fallbacks.properties
19	heuristicSelection.loopConfig	components/svcomp23--multipleLoopsConfig.properties
20	heuristicSelection.loopFreeConfig	components/svcomp23--configselection-restart-bmc-fallbacks.properties
21	heuristicSelection.singleLoopConfig	components/svcomp23--singleLoopConfig.properties
22	language	C
23	limits.time.cpu	900s
24	limits.time.cpu::required	900
25	log.level	INFO
26	memorycleanup.config	svcomp23--memorycleanup.properties
27	memorysafety.config	svcomp23--memorysafety.properties
28	overflow.config	svcomp23--overflow.properties
29	parser.usePreprocessor	true
30	specification	/home/artjom/CPAchecker-2.2-unix/config/properties/unreach-call.prp
31	statistics.print	true
32	termination.config	svcomp23--termination.properties
33	termination.violation.witness	witness.graphml

About

This table was generated by CPAchecker. For feedback, questions, and bug reports please use our issue tracker.

License: Apache 2.0 License

This application includes third-party dependencies under different licenses. Click here to view them.

Source: {{dependency.repository}}

License:

Full text of license

{{dependencies.licenses[dependency.licenseId]}}

Report for no_context/combo2.c

About

{{dependency.name}} {{dependency.version}}

1	// Automatically generated by cegarmc
2	//
3
4
5	extern void __VERIFIER_assume(int);
6	extern int __VERIFIER_nondet_bool();
7	extern char __VERIFIER_nondet_char();
8	extern signed char __VERIFIER_nondet_schar();
9	extern unsigned char __VERIFIER_nondet_uchar();
10	extern int __VERIFIER_nondet_int();
11	extern unsigned int __VERIFIER_nondet_uint();
12	extern short __VERIFIER_nondet_short();
13	extern unsigned short __VERIFIER_nondet_ushort();
14	extern long __VERIFIER_nondet_long();
15	extern unsigned long __VERIFIER_nondet_ulong();
16	extern long long __VERIFIER_nondet_longlong();
17	extern unsigned long long __VERIFIER_nondet_ull();
18	extern float __VERIFIER_nondet_float();
19	extern double __VERIFIER_nondet_double();
20	extern long double __VERIFIER_nondet_longdouble();
21	extern void * __VERIFIER_nondet_pointer();
22
23	int D_print_i;
24	int D_print_st;
25	int D_z;
26	int N_generate_i;
27	int N_generate_st;
28	int S1_addsub_i;
29	int S1_addsub_st;
30	int S2_presdbl_i;
31	int S2_presdbl_st;
32	int S3_zero_i;
33	int S3_zero_st;
34	int count;
35	int main_clk_ev;
36	int main_clk_neg_edge;
37	int main_clk_pos_edge;
38	int main_clk_req_up;
39	int main_clk_val;
40	int main_clk_val_t;
41	int main_dbl_ev;
42	int main_dbl_req_up;
43	int main_dbl_val;
44	int main_dbl_val_t;
45	int main_diff_ev;
46	int main_diff_req_up;
47	int main_diff_val;
48	int main_diff_val_t;
49	int main_in1_ev;
50	int main_in1_req_up;
51	int main_in1_val;
52	int main_in1_val_t;
53	int main_in2_ev;
54	int main_in2_req_up;
55	int main_in2_val;
56	int main_in2_val_t;
57	int main_pres_ev;
58	int main_pres_req_up;
59	int main_pres_val;
60	int main_pres_val_t;
61	int main_sum_ev;
62	int main_sum_req_up;
63	int main_sum_val;
64	int main_sum_val_t;
65	int main_zero_ev;
66	int main_zero_req_up;
67	int main_zero_val;
68	int main_zero_val_t;
69	int modFlag;
70	int res;
71
72	void error();
73	void N_generate();
74	void S1_addsub();
75	void S2_presdbl();
76	void S3_zero();
77	void D_print();
78	void eval();
79	void start_simulation();
80
81
82	void error() {
83	{
84	goto ERROR;
85	ERROR: ;
86	return;
87	}
88	}
89
90	void N_generate() {
91	auto int a;
92	auto int b;
93	{
94	main_in1_val_t = __VERIFIER_nondet_int();
95	main_in1_req_up = 1;
96	main_in2_val_t = __VERIFIER_nondet_int();
97	main_in2_req_up = 1;
98	return;
99	}
100	}
101
102	void S1_addsub() {
103	auto int a;
104	auto int b;
105	{
106	a = main_in1_val;
107	b = main_in2_val;
108	main_sum_val_t = a + b;
109	main_sum_req_up = 1;
110	main_diff_val_t = a - b;
111	main_diff_req_up = 1;
112	return;
113	}
114	}
115
116	void S2_presdbl() {
117	auto int a;
118	auto int b;
119	auto int c;
120	auto int d;
121	{
122	a = main_sum_val;
123	b = main_diff_val;
124	main_pres_val_t = a;
125	main_pres_req_up = 1;
126	c = a + b;
127	d = a - b;
128	main_dbl_val_t = c + d;
129	main_dbl_req_up = 1;
130	return;
131	}
132	}
133
134	void S3_zero() {
135	auto int a;
136	auto int b;
137	{
138	a = main_pres_val;
139	b = main_dbl_val;
140	main_zero_val_t = b - (a + a);
141	main_zero_req_up = 1;
142	return;
143	}
144	}
145
146	void D_print() {
147	{
148	D_z = main_zero_val;
149	return;
150	}
151	}
152
153	void eval() {
154	auto int tmp;
155	auto int tmp___0;
156	auto int tmp___1;
157	auto int tmp___2;
158	auto int tmp___3;
159	{
160	{
161	while (1) {
162	{
163	while_0_continue: ;
164	if (N_generate_st == 0) {
165	}
166	else {
167	if (S1_addsub_st == 0) {
168	}
169	else {
170	if (S2_presdbl_st == 0) {
171	}
172	else {
173	if (S3_zero_st == 0) {
174	}
175	else {
176	if (D_print_st == 0) {
177	}
178	else {
179	goto while_0_break;
180	}
181	}
182	}
183	}
184	}
185	if (N_generate_st == 0) {
186	{
187	tmp = __VERIFIER_nondet_int();
188	}
189	if (tmp) {
190	N_generate_st = 1;
191	N_generate();
192	}
193	else {
194	}
195	}
196	else {
197	}
198	if (S1_addsub_st == 0) {
199	{
200	tmp___0 = __VERIFIER_nondet_int();
201	}
202	if (tmp___0) {
203	S1_addsub_st = 1;
204	S1_addsub();
205	}
206	else {
207	}
208	}
209	else {
210	}
211	if (S2_presdbl_st == 0) {
212	{
213	tmp___1 = __VERIFIER_nondet_int();
214	}
215	if (tmp___1) {
216	S2_presdbl_st = 1;
217	S2_presdbl();
218	}
219	else {
220	}
221	}
222	else {
223	}
224	if (S3_zero_st == 0) {
225	{
226	tmp___2 = __VERIFIER_nondet_int();
227	}
228	if (tmp___2) {
229	S3_zero_st = 1;
230	S3_zero();
231	}
232	else {
233	}
234	}
235	else {
236	}
237	if (D_print_st == 0) {
238	{
239	tmp___3 = __VERIFIER_nondet_int();
240	}
241	if (tmp___3) {
242	D_print_st = 1;
243	D_print();
244	}
245	else {
246	}
247	}
248	else {
249	}
250	}
251	}
252	while_0_break: ;
253	}
254	return;
255	}
256	}
257
258	void start_simulation() {
259	auto int kernel_st;
260	{
261	kernel_st = 0;
262	if (main_in1_req_up == 1) {
263	if (main_in1_val != main_in1_val_t) {
264	main_in1_val = main_in1_val_t;
265	main_in1_ev = 0;
266	}
267	else {
268	}
269	main_in1_req_up = 0;
270	}
271	else {
272	}
273	if (main_in2_req_up == 1) {
274	if (main_in2_val != main_in2_val_t) {
275	main_in2_val = main_in2_val_t;
276	main_in2_ev = 0;
277	}
278	else {
279	}
280	main_in2_req_up = 0;
281	}
282	else {
283	}
284	if (main_sum_req_up == 1) {
285	if (main_sum_val != main_sum_val_t) {
286	main_sum_val = main_sum_val_t;
287	main_sum_ev = 0;
288	}
289	else {
290	}
291	main_sum_req_up = 0;
292	}
293	else {
294	}
295	if (main_diff_req_up == 1) {
296	if (main_diff_val != main_diff_val_t) {
297	main_diff_val = main_diff_val_t;
298	main_diff_ev = 0;
299	}
300	else {
301	}
302	main_diff_req_up = 0;
303	}
304	else {
305	}
306	if (main_pres_req_up == 1) {
307	if (main_pres_val != main_pres_val_t) {
308	main_pres_val = main_pres_val_t;
309	main_pres_ev = 0;
310	}
311	else {
312	}
313	main_pres_req_up = 0;
314	}
315	else {
316	}
317	if (main_dbl_req_up == 1) {
318	if (main_dbl_val != main_dbl_val_t) {
319	main_dbl_val = main_dbl_val_t;
320	main_dbl_ev = 0;
321	}
322	else {
323	}
324	main_dbl_req_up = 0;
325	}
326	else {
327	}
328	if (main_zero_req_up == 1) {
329	if (main_zero_val != main_zero_val_t) {
330	main_zero_val = main_zero_val_t;
331	main_zero_ev = 0;
332	}
333	else {
334	}
335	main_zero_req_up = 0;
336	}
337	else {
338	}
339	if (main_clk_req_up == 1) {
340	if (main_clk_val != main_clk_val_t) {
341	main_clk_val = main_clk_val_t;
342	main_clk_ev = 0;
343	if (main_clk_val == 1) {
344	main_clk_pos_edge = 0;
345	main_clk_neg_edge = 2;
346	}
347	else {
348	main_clk_neg_edge = 0;
349	main_clk_pos_edge = 2;
350	}
351	}
352	else {
353	}
354	main_clk_req_up = 0;
355	}
356	else {
357	}
358	if (N_generate_i == 1) {
359	N_generate_st = 0;
360	}
361	else {
362	N_generate_st = 2;
363	}
364	if (S1_addsub_i == 1) {
365	S1_addsub_st = 0;
366	}
367	else {
368	S1_addsub_st = 2;
369	}
370	if (S2_presdbl_i == 1) {
371	S2_presdbl_st = 0;
372	}
373	else {
374	S2_presdbl_st = 2;
375	}
376	if (S3_zero_i == 1) {
377	S3_zero_st = 0;
378	}
379	else {
380	S3_zero_st = 2;
381	}
382	if (D_print_i == 1) {
383	D_print_st = 0;
384	}
385	else {
386	D_print_st = 2;
387	}
388	if (main_in1_ev == 0) {
389	main_in1_ev = 1;
390	}
391	else {
392	}
393	if (main_in2_ev == 0) {
394	main_in2_ev = 1;
395	}
396	else {
397	}
398	if (main_sum_ev == 0) {
399	main_sum_ev = 1;
400	}
401	else {
402	}
403	if (main_diff_ev == 0) {
404	main_diff_ev = 1;
405	}
406	else {
407	}
408	if (main_pres_ev == 0) {
409	main_pres_ev = 1;
410	}
411	else {
412	}
413	if (main_dbl_ev == 0) {
414	main_dbl_ev = 1;
415	}
416	else {
417	}
418	if (main_zero_ev == 0) {
419	main_zero_ev = 1;
420	}
421	else {
422	}
423	if (main_clk_ev == 0) {
424	main_clk_ev = 1;
425	}
426	else {
427	}
428	if (main_clk_pos_edge == 0) {
429	main_clk_pos_edge = 1;
430	}
431	else {
432	}
433	if (main_clk_neg_edge == 0) {
434	main_clk_neg_edge = 1;
435	}
436	else {
437	}
438	if (main_clk_pos_edge == 1) {
439	N_generate_st = 0;
440	}
441	else {
442	}
443	if (main_clk_pos_edge == 1) {
444	S1_addsub_st = 0;
445	}
446	else {
447	}
448	if (main_clk_pos_edge == 1) {
449	S2_presdbl_st = 0;
450	}
451	else {
452	}
453	if (main_clk_pos_edge == 1) {
454	S3_zero_st = 0;
455	}
456	else {
457	}
458	if (main_clk_pos_edge == 1) {
459	D_print_st = 0;
460	}
461	else {
462	}
463	if (main_in1_ev == 1) {
464	main_in1_ev = 2;
465	}
466	else {
467	}
468	if (main_in2_ev == 1) {
469	main_in2_ev = 2;
470	}
471	else {
472	}
473	if (main_sum_ev == 1) {
474	main_sum_ev = 2;
475	}
476	else {
477	}
478	if (main_diff_ev == 1) {
479	main_diff_ev = 2;
480	}
481	else {
482	}
483	if (main_pres_ev == 1) {
484	main_pres_ev = 2;
485	}
486	else {
487	}
488	if (main_dbl_ev == 1) {
489	main_dbl_ev = 2;
490	}
491	else {
492	}
493	if (main_zero_ev == 1) {
494	main_zero_ev = 2;
495	}
496	else {
497	}
498	if (main_clk_ev == 1) {
499	main_clk_ev = 2;
500	}
501	else {
502	}
503	if (main_clk_pos_edge == 1) {
504	main_clk_pos_edge = 2;
505	}
506	else {
507	}
508	if (main_clk_neg_edge == 1) {
509	main_clk_neg_edge = 2;
510	}
511	else {
512	}
513	{
514	while (1) {
515	{
516	while_1_continue: ;
517	{
518	kernel_st = 1;
519	eval();
520	}
521	kernel_st = 2;
522	if (main_in1_req_up == 1) {
523	if (main_in1_val != main_in1_val_t) {
524	main_in1_val = main_in1_val_t;
525	main_in1_ev = 0;
526	}
527	else {
528	}
529	main_in1_req_up = 0;
530	}
531	else {
532	}
533	if (main_in2_req_up == 1) {
534	if (main_in2_val != main_in2_val_t) {
535	main_in2_val = main_in2_val_t;
536	main_in2_ev = 0;
537	}
538	else {
539	}
540	main_in2_req_up = 0;
541	}
542	else {
543	}
544	if (main_sum_req_up == 1) {
545	if (main_sum_val != main_sum_val_t) {
546	main_sum_val = main_sum_val_t;
547	main_sum_ev = 0;
548	}
549	else {
550	}
551	main_sum_req_up = 0;
552	}
553	else {
554	}
555	if (main_diff_req_up == 1) {
556	if (main_diff_val != main_diff_val_t) {
557	main_diff_val = main_diff_val_t;
558	main_diff_ev = 0;
559	}
560	else {
561	}
562	main_diff_req_up = 0;
563	}
564	else {
565	}
566	if (main_pres_req_up == 1) {
567	if (main_pres_val != main_pres_val_t) {
568	main_pres_val = main_pres_val_t;
569	main_pres_ev = 0;
570	}
571	else {
572	}
573	main_pres_req_up = 0;
574	}
575	else {
576	}
577	if (main_dbl_req_up == 1) {
578	if (main_dbl_val != main_dbl_val_t) {
579	main_dbl_val = main_dbl_val_t;
580	main_dbl_ev = 0;
581	}
582	else {
583	}
584	main_dbl_req_up = 0;
585	}
586	else {
587	}
588	if (main_zero_req_up == 1) {
589	if (main_zero_val != main_zero_val_t) {
590	main_zero_val = main_zero_val_t;
591	main_zero_ev = 0;
592	}
593	else {
594	}
595	main_zero_req_up = 0;
596	}
597	else {
598	}
599	if (main_clk_req_up == 1) {
600	if (main_clk_val != main_clk_val_t) {
601	main_clk_val = main_clk_val_t;
602	main_clk_ev = 0;
603	if (main_clk_val == 1) {
604	main_clk_pos_edge = 0;
605	main_clk_neg_edge = 2;
606	}
607	else {
608	main_clk_neg_edge = 0;
609	main_clk_pos_edge = 2;
610	}
611	}
612	else {
613	}
614	main_clk_req_up = 0;
615	}
616	else {
617	}
618	kernel_st = 3;
619	if (main_in1_ev == 0) {
620	main_in1_ev = 1;
621	}
622	else {
623	}
624	if (main_in2_ev == 0) {
625	main_in2_ev = 1;
626	}
627	else {
628	}
629	if (main_sum_ev == 0) {
630	main_sum_ev = 1;
631	}
632	else {
633	}
634	if (main_diff_ev == 0) {
635	main_diff_ev = 1;
636	}
637	else {
638	}
639	if (main_pres_ev == 0) {
640	main_pres_ev = 1;
641	}
642	else {
643	}
644	if (main_dbl_ev == 0) {
645	main_dbl_ev = 1;
646	}
647	else {
648	}
649	if (main_zero_ev == 0) {
650	main_zero_ev = 1;
651	}
652	else {
653	}
654	if (main_clk_ev == 0) {
655	main_clk_ev = 1;
656	}
657	else {
658	}
659	if (main_clk_pos_edge == 0) {
660	main_clk_pos_edge = 1;
661	}
662	else {
663	}
664	if (main_clk_neg_edge == 0) {
665	main_clk_neg_edge = 1;
666	}
667	else {
668	}
669	if (main_clk_pos_edge == 1) {
670	N_generate_st = 0;
671	}
672	else {
673	}
674	if (main_clk_pos_edge == 1) {
675	S1_addsub_st = 0;
676	}
677	else {
678	}
679	if (main_clk_pos_edge == 1) {
680	S2_presdbl_st = 0;
681	}
682	else {
683	}
684	if (main_clk_pos_edge == 1) {
685	S3_zero_st = 0;
686	}
687	else {
688	}
689	if (main_clk_pos_edge == 1) {
690	D_print_st = 0;
691	}
692	else {
693	}
694	if (main_in1_ev == 1) {
695	main_in1_ev = 2;
696	}
697	else {
698	}
699	if (main_in2_ev == 1) {
700	main_in2_ev = 2;
701	}
702	else {
703	}
704	if (main_sum_ev == 1) {
705	main_sum_ev = 2;
706	}
707	else {
708	}
709	if (main_diff_ev == 1) {
710	main_diff_ev = 2;
711	}
712	else {
713	}
714	if (main_pres_ev == 1) {
715	main_pres_ev = 2;
716	}
717	else {
718	}
719	if (main_dbl_ev == 1) {
720	main_dbl_ev = 2;
721	}
722	else {
723	}
724	if (main_zero_ev == 1) {
725	main_zero_ev = 2;
726	}
727	else {
728	}
729	if (main_clk_ev == 1) {
730	main_clk_ev = 2;
731	}
732	else {
733	}
734	if (main_clk_pos_edge == 1) {
735	main_clk_pos_edge = 2;
736	}
737	else {
738	}
739	if (main_clk_neg_edge == 1) {
740	main_clk_neg_edge = 2;
741	}
742	else {
743	}
744	if (N_generate_st == 0) {
745	}
746	else {
747	if (S1_addsub_st == 0) {
748	}
749	else {
750	if (S2_presdbl_st == 0) {
751	}
752	else {
753	if (S3_zero_st == 0) {
754	}
755	else {
756	if (D_print_st == 0) {
757	}
758	else {
759	goto while_1_break;
760	}
761	}
762	}
763	}
764	}
765	}
766	}
767	while_1_break: ;
768	}
769	return;
770	}
771	}
772
773	void main () {
774	//
775	// Number of lvals: 62
776	// Frama_C_interval: int (int min, int max)
777	// int (int min, int max)
778	// error: void (void)
779	// void (void)
780	// count: int
781	// int
782	// res: int
783	// int
784	// modFlag: int
785	// int
786	// main_in1_val: int
787	// int
788	// main_in1_val_t: int
789	// int
790	// main_in1_ev: int
791	// int
792	// main_in1_req_up: int
793	// int
794	// main_in2_val: int
795	// int
796	// main_in2_val_t: int
797	// int
798	// main_in2_ev: int
799	// int
800	// main_in2_req_up: int
801	// int
802	// main_diff_val: int
803	// int
804	// main_diff_val_t: int
805	// int
806	// main_diff_ev: int
807	// int
808	// main_diff_req_up: int
809	// int
810	// main_sum_val: int
811	// int
812	// main_sum_val_t: int
813	// int
814	// main_sum_ev: int
815	// int
816	// main_sum_req_up: int
817	// int
818	// main_pres_val: int
819	// int
820	// main_pres_val_t: int
821	// int
822	// main_pres_ev: int
823	// int
824	// main_pres_req_up: int
825	// int
826	// main_dbl_val: int
827	// int
828	// main_dbl_val_t: int
829	// int
830	// main_dbl_ev: int
831	// int
832	// main_dbl_req_up: int
833	// int
834	// main_zero_val: int
835	// int
836	// main_zero_val_t: int
837	// int
838	// main_zero_ev: int
839	// int
840	// main_zero_req_up: int
841	// int
842	// main_clk_val: int
843	// int
844	// main_clk_val_t: int
845	// int
846	// main_clk_ev: int
847	// int
848	// main_clk_req_up: int
849	// int
850	// main_clk_pos_edge: int
851	// int
852	// main_clk_neg_edge: int
853	// int
854	// N_generate_st: int
855	// int
856	// N_generate_i: int
857	// int
858	// S1_addsub_st: int
859	// int
860	// S1_addsub_i: int
861	// int
862	// S2_presdbl_st: int
863	// int
864	// S2_presdbl_i: int
865	// int
866	// S3_zero_st: int
867	// int
868	// S3_zero_i: int
869	// int
870	// D_z: int
871	// int
872	// D_print_st: int
873	// int
874	// D_print_i: int
875	// int
876	// N_generate: void (void)
877	// void (void)
878	// S1_addsub: void (void)
879	// void (void)
880	// S2_presdbl: void (void)
881	// void (void)
882	// S3_zero: void (void)
883	// void (void)
884	// D_print: void (void)
885	// void (void)
886	// eval: void (void)
887	// void (void)
888	// start_simulation: void (void)
889	// void (void)
890	// n1: int
891	// int
892	// n2: int
893	// int
894	// n3: int
895	// int
896	// bound: int
897	// int
898	// i: int
899	// int
900	//
901
902	D_print_i = __VERIFIER_nondet_int();
903	D_print_st = __VERIFIER_nondet_int();
904	D_z = __VERIFIER_nondet_int();
905	N_generate_i = __VERIFIER_nondet_int();
906	N_generate_st = __VERIFIER_nondet_int();
907	S1_addsub_i = __VERIFIER_nondet_int();
908	S1_addsub_st = __VERIFIER_nondet_int();
909	S2_presdbl_i = __VERIFIER_nondet_int();
910	S2_presdbl_st = __VERIFIER_nondet_int();
911	S3_zero_i = __VERIFIER_nondet_int();
912	S3_zero_st = __VERIFIER_nondet_int();
913	count = __VERIFIER_nondet_int();
914	main_clk_ev = __VERIFIER_nondet_int();
915	main_clk_neg_edge = __VERIFIER_nondet_int();
916	main_clk_pos_edge = __VERIFIER_nondet_int();
917	main_clk_req_up = __VERIFIER_nondet_int();
918	main_clk_val = __VERIFIER_nondet_int();
919	main_clk_val_t = __VERIFIER_nondet_int();
920	main_dbl_ev = __VERIFIER_nondet_int();
921	main_dbl_req_up = __VERIFIER_nondet_int();
922	main_dbl_val = __VERIFIER_nondet_int();
923	main_dbl_val_t = __VERIFIER_nondet_int();
924	main_diff_ev = __VERIFIER_nondet_int();
925	main_diff_req_up = __VERIFIER_nondet_int();
926	main_diff_val = __VERIFIER_nondet_int();
927	main_diff_val_t = __VERIFIER_nondet_int();
928	main_in1_ev = __VERIFIER_nondet_int();
929	main_in1_req_up = __VERIFIER_nondet_int();
930	main_in1_val = __VERIFIER_nondet_int();
931	main_in1_val_t = __VERIFIER_nondet_int();
932	main_in2_ev = __VERIFIER_nondet_int();
933	main_in2_req_up = __VERIFIER_nondet_int();
934	main_in2_val = __VERIFIER_nondet_int();
935	main_in2_val_t = __VERIFIER_nondet_int();
936	main_pres_ev = __VERIFIER_nondet_int();
937	main_pres_req_up = __VERIFIER_nondet_int();
938	main_pres_val = __VERIFIER_nondet_int();
939	main_pres_val_t = __VERIFIER_nondet_int();
940	main_sum_ev = __VERIFIER_nondet_int();
941	main_sum_req_up = __VERIFIER_nondet_int();
942	main_sum_val = __VERIFIER_nondet_int();
943	main_sum_val_t = __VERIFIER_nondet_int();
944	main_zero_ev = __VERIFIER_nondet_int();
945	main_zero_req_up = __VERIFIER_nondet_int();
946	main_zero_val = __VERIFIER_nondet_int();
947	main_zero_val_t = __VERIFIER_nondet_int();
948	modFlag = __VERIFIER_nondet_int();
949	res = __VERIFIER_nondet_int();
950
951
952
953	{
954	int n1 = 3;
955	int n2 = 5;
956	int n3 = 7;
957	res = 0;
958	auto int bound;
959	bound = __VERIFIER_nondet_int();
960	{
961	int i = 0;
962	while (1) {
963	if (i < bound) {
964	}
965	else {
966	break;
967	}
968	{
969	if (i % n1 == 0) {
970	if (i % n2 == 0) {
971	if (i % n3 == 0) {
972	res = i;
973	}
974	else {
975	}
976	}
977	else {
978	}
979	}
980	else {
981	}
982	}
983	i ++;
984	}
985	}
986	{
987	modFlag = res;
988	}
989	if (modFlag % 105 == 0) {
990	{
991	count = 0;
992	main_in1_ev = 2;
993	main_in1_req_up = 0;
994	main_in2_ev = 2;
995	main_in2_req_up = 0;
996	main_diff_ev = 2;
997	main_diff_req_up = 0;
998	main_sum_ev = 2;
999	main_sum_req_up = 0;
1000	main_pres_ev = 2;
1001	main_pres_req_up = 0;
1002	main_dbl_ev = 2;
1003	main_dbl_req_up = 0;
1004	main_zero_ev = 2;
1005	main_zero_req_up = 0;
1006	main_clk_val = 0;
1007	main_clk_ev = 2;
1008	main_clk_req_up = 0;
1009	main_clk_pos_edge = 2;
1010	main_clk_neg_edge = 2;
1011	count = 0;
1012	N_generate_i = 0;
1013	S1_addsub_i = 0;
1014	S2_presdbl_i = 0;
1015	S3_zero_i = 0;
1016	D_print_i = 0;
1017	start_simulation();
1018	}
1019	{
1020	while (1) {
1021	{
1022	while_2_continue: ;
1023	{
1024	main_clk_val_t = 1;
1025	main_clk_req_up = 1;
1026	start_simulation();
1027	count ++;
1028	}
1029	if (count == 5) {
1030	if (! (D_z == 0)) {
1031	error();
1032	}
1033	else {
1034	}
1035	count = 0;
1036	}
1037	else {
1038	}
1039	{
1040	main_clk_val_t = 0;
1041	main_clk_req_up = 1;
1042	start_simulation();
1043	}
1044	}
1045	}
1046	}
1047	}
1048	else {
1049	error();
1050	}
1051	}
1052	return;
1053	}